(* Title: thys/Turing.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Turing Machines›

theory Turing
  imports Main
begin

section ‹Basic definitions of Turing machine›

datatype action = W0 | W1 | L | R | Nop

datatype cell = Bk | Oc

type_synonym tape = "cell list × cell list"

type_synonym state = nat

type_synonym instr = "action × state"

type_synonym tprog = "instr list × nat"

type_synonym tprog0 = "instr list"

type_synonym config = "state × tape"

fun nth_of where
  "nth_of xs i = (if i ≥ length xs then None else Some (xs ! i))"

lemma nth_of_map [simp]:
  shows "nth_of (map f p) n = (case (nth_of p n) of None ⇒ None | Some x ⇒ Some (f x))"
  by simp

fun 
  fetch :: "instr list ⇒ state ⇒ cell ⇒ instr"
  where
    "fetch p 0 b = (Nop, 0)"
  | "fetch p (Suc s) Bk = 
     (case nth_of p (2 * s) of
        Some i ⇒ i
      | None ⇒ (Nop, 0))"
  |"fetch p (Suc s) Oc = 
     (case nth_of p ((2 * s) + 1) of
         Some i ⇒ i
       | None ⇒ (Nop, 0))"

lemma fetch_Nil [simp]:
  shows "fetch [] s b = (Nop, 0)"
  by (cases s,force) (cases b;force)

fun 
  update :: "action ⇒ tape ⇒ tape"
  where 
    "update W0 (l, r) = (l, Bk # (tl r))" 
  | "update W1 (l, r) = (l, Oc # (tl r))"
  | "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" 
  | "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" 
  | "update Nop (l, r) = (l, r)"

abbreviation 
  "read r == if (r = []) then Bk else hd r"

fun step :: "config ⇒ tprog ⇒ config"
  where 
    "step (s, l, r) (p, off) = 
     (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"

abbreviation
  "step0 c p ≡ step c (p, 0)"

fun steps :: "config ⇒ tprog ⇒ nat ⇒ config"
  where
    "steps c p 0 = c" |
    "steps c p (Suc n) = steps (step c p) p n"

abbreviation
  "steps0 c p n ≡ steps c (p, 0) n"

lemma step_red [simp]: 
  shows "steps c p (Suc n) = step (steps c p n) p"
  by (induct n arbitrary: c) (auto)

lemma steps_add [simp]: 
  shows "steps c p (m + n) = steps (steps c p m) p n"
  by (induct m arbitrary: c) (auto)

lemma step_0 [simp]: 
  shows "step (0, (l, r)) p = (0, (l, r))"
  by (cases p, simp)

lemma steps_0 [simp]: 
  shows "steps (0, (l, r)) p n = (0, (l, r))"
  by (induct n) (simp_all)

fun
  is_final :: "config ⇒ bool"
  where
    "is_final (s, l, r) = (s = 0)"

lemma is_final_eq: 
  shows "is_final (s, tp) = (s = 0)"
  by (cases tp) (auto)

lemma is_finalI [intro]:
  shows "is_final (0, tp)"
  by (simp add: is_final_eq)

lemma after_is_final:
  assumes "is_final c"
  shows "is_final (steps c p n)"
  using assms 
  by(induct n;cases c;auto)

lemma is_final:
  assumes a: "is_final (steps c p n1)"
    and b: "n1 ≤ n2"
  shows "is_final (steps c p n2)"
proof - 
  obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add)
  from a show "is_final (steps c p n2)" unfolding eq
    by (simp add: after_is_final)
qed

lemma not_is_final:
  assumes a: "¬ is_final (steps c p n1)"
    and b: "n2 ≤ n1"
  shows "¬ is_final (steps c p n2)"
proof (rule notI)
  obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add)
  assume "is_final (steps c p n2)"
  then have "is_final (steps c p n1)" unfolding eq
    by (simp add: after_is_final)
  with a show "False" by simp
qed

(* if the machine is in the halting state, there must have 
   been a state just before the halting state *)
lemma before_final: 
  assumes "steps0 (1, tp) A n = (0, tp')"
  shows "∃ n'. ¬ is_final (steps0 (1, tp) A n') ∧ steps0 (1, tp) A (Suc n') = (0, tp')"
  using assms
proof(induct n arbitrary: tp')
  case (0 tp')
  have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
  then show "∃n'. ¬ is_final (steps0 (1, tp) A n') ∧ steps0 (1, tp) A (Suc n') = (0, tp')"
    by simp
next
  case (Suc n tp')
  have ih: "⋀tp'. steps0 (1, tp) A n = (0, tp') ⟹
    ∃n'. ¬ is_final (steps0 (1, tp) A n') ∧ steps0 (1, tp) A (Suc n') = (0, tp')" by fact
  have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
  obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
    by (auto intro: is_final.cases)
  then show "∃n'. ¬ is_final (steps0 (1, tp) A n') ∧ steps0 (1, tp) A (Suc n') = (0, tp')"
  proof (cases "s = 0")
    case True (* in halting state *)
    then have "steps0 (1, tp) A n = (0, tp')"
      using asm cases by (simp del: steps.simps)
    then show ?thesis using ih by simp
  next
    case False (* not in halting state *)
    then have "¬ is_final (steps0 (1, tp) A n) ∧ steps0 (1, tp) A (Suc n) = (0, tp')"
      using asm cases by simp
    then show ?thesis by auto
  qed
qed

lemma least_steps: 
  assumes "steps0 (1, tp) A n = (0, tp')"
  shows "∃ n'. (∀n'' < n'. ¬ is_final (steps0 (1, tp) A n'')) ∧ 
               (∀n'' ≥ n'. is_final (steps0 (1, tp) A n''))"
proof -
  from before_final[OF assms] 
  obtain n' where
    before: "¬ is_final (steps0 (1, tp) A n')" and
    final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto
  from before
  have "∀n'' < Suc n'. ¬ is_final (steps0 (1, tp) A n'')"
    using not_is_final by auto
  moreover
  from final 
  have "∀n'' ≥ Suc n'. is_final (steps0 (1, tp) A n'')" 
    using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq)
  ultimately
  show "∃ n'. (∀n'' < n'. ¬ is_final (steps0 (1, tp) A n'')) ∧ (∀n'' ≥ n'. is_final (steps0 (1, tp) A n''))"
    by blast
qed



(* well-formedness of Turing machine programs *)
abbreviation "is_even n ≡ (n::nat) mod 2 = 0"

fun 
  tm_wf :: "tprog ⇒ bool"
  where
    "tm_wf (p, off) = (length p ≥ 2 ∧ is_even (length p) ∧ 
                    (∀(a, s) ∈ set p. s ≤ length p div 2 + off ∧ s ≥ off))"

abbreviation
  "tm_wf0 p ≡ tm_wf (p, 0)"

abbreviation exponent :: "'a ⇒ nat ⇒ 'a list" ("_ ↑ _" [100, 99] 100)
  where "x ↑ n == replicate n x"

lemma hd_repeat_cases:
  "P (hd (a ↑ m @ r)) ⟷ (m = 0 ⟶ P (hd r)) ∧ (∀nat. m = Suc nat ⟶ P a)"
  by (cases m,auto)

class tape =
  fixes tape_of :: "'a ⇒ cell list" ("<_>" 100)


instantiation nat::tape begin
definition tape_of_nat where "tape_of_nat (n::nat) ≡ Oc ↑ (Suc n)"
instance by standard
end

type_synonym nat_list = "nat list"

instantiation list::(tape) tape begin
fun tape_of_nat_list :: "('a::tape) list ⇒ cell list" 
  where 
    "tape_of_nat_list [] = []" |
    "tape_of_nat_list [n] = <n>" |
    "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
definition tape_of_list where "tape_of_list ≡ tape_of_nat_list"
instance by standard
end

instantiation prod:: (tape, tape) tape begin
fun tape_of_nat_prod :: "('a::tape) × ('b::tape) ⇒ cell list" 
  where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>" 
definition tape_of_prod where "tape_of_prod ≡ tape_of_nat_prod"
instance by standard
end

fun 
  shift :: "instr list ⇒ nat ⇒ instr list"
  where
    "shift p n = (map (λ (a, s). (a, (if s = 0 then 0 else s + n))) p)"

fun 
  adjust :: "instr list ⇒ nat ⇒ instr list"
  where
    "adjust p e = map (λ (a, s). (a, if s = 0 then e else s)) p"

abbreviation
  "adjust0 p ≡ adjust p (Suc (length p div 2))"

lemma length_shift [simp]: 
  shows "length (shift p n) = length p"
  by simp

lemma length_adjust [simp]: 
  shows "length (adjust p n) = length p"
  by (induct p) (auto)


(* composition of two Turing machines *)
fun
  tm_comp :: "instr list ⇒ instr list ⇒ instr list" ("_ |+| _" [0, 0] 100)
  where
    "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"

lemma tm_comp_length:
  shows "length (A |+| B) = length A + length B"
  by auto

lemma tm_comp_wf[intro]: 
  "⟦tm_wf (A, 0); tm_wf (B, 0)⟧ ⟹ tm_wf (A |+| B, 0)"
  by (fastforce)

lemma tm_comp_step: 
  assumes unfinal: "¬ is_final (step0 c A)"
  shows "step0 c (A |+| B) = step0 c A"
proof -
  obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) 
  have "¬ is_final (step0 (s, l, r) A)" using unfinal eq by simp
  then have "case (fetch A s (read r)) of (a, s) ⇒ s ≠ 0"
    by (auto simp add: is_final_eq)
  then have "fetch (A |+| B) s (read r) = fetch A s (read r)"
    apply (cases "read r";cases s)
    by (auto simp: tm_comp_length nth_append)
  then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) 
qed

lemma tm_comp_steps:  
  assumes "¬ is_final (steps0 c A n)" 
  shows "steps0 c (A |+| B) n = steps0 c A n"
  using assms
proof(induct n)
  case 0
  then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto
next 
  case (Suc n)
  have ih: "¬ is_final (steps0 c A n) ⟹ steps0 c (A |+| B) n = steps0 c A n" by fact
  have fin: "¬ is_final (steps0 c A (Suc n))" by fact
  then have fin1: "¬ is_final (step0 (steps0 c A n) A)" 
    by (auto simp only: step_red)
  then have fin2: "¬ is_final (steps0 c A n)"
    by (metis is_final_eq step_0 surj_pair) 

  have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" 
    by (simp only: step_red)
  also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2])
  also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1])
  finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)"
    by (simp only: step_red)
qed

lemma tm_comp_fetch_in_A:
  assumes h1: "fetch A s x = (a, 0)"
    and h2: "s ≤ length A div 2" 
    and h3: "s ≠ 0"
  shows "fetch (A |+| B) s x = (a, Suc (length A div 2))"
  using h1 h2 h3
  apply(cases s;cases x)
  by(auto simp: tm_comp_length nth_append)

lemma tm_comp_exec_after_first:
  assumes h1: "¬ is_final c" 
    and h2: "step0 c A = (0, tp)"
    and h3: "fst c ≤ length A div 2"
  shows "step0 c (A |+| B) = (Suc (length A div 2), tp)"
  using h1 h2 h3
  apply(case_tac c)
  apply(auto simp del: tm_comp.simps)
   apply(case_tac "fetch A a Bk")
   apply(simp del: tm_comp.simps)
   apply(subst tm_comp_fetch_in_A;force)
  apply(case_tac "fetch A a (hd ca)")
  apply(simp del: tm_comp.simps)
  apply(subst tm_comp_fetch_in_A)
     apply(auto)[4]
  done

lemma step_in_range: 
  assumes h1: "¬ is_final (step0 c A)"
    and h2: "tm_wf (A, 0)"
  shows "fst (step0 c A) ≤ length A div 2"
  using h1 h2
  apply(cases c;cases "fst c";cases "hd (snd (snd c))")
  by(auto simp add: Let_def case_prod_beta')

lemma steps_in_range: 
  assumes h1: "¬ is_final (steps0 (1, tp) A stp)"
    and h2: "tm_wf (A, 0)"
  shows "fst (steps0 (1, tp) A stp) ≤ length A div 2"
  using h1
proof(induct stp)
  case 0
  then show "fst (steps0 (1, tp) A 0) ≤ length A div 2" using h2
    by (auto)
next
  case (Suc stp)
  have ih: "¬ is_final (steps0 (1, tp) A stp) ⟹ fst (steps0 (1, tp) A stp) ≤ length A div 2" by fact
  have h: "¬ is_final (steps0 (1, tp) A (Suc stp))" by fact
  from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) ≤ length A div 2"
    by (metis step_in_range step_red)
qed

(* if A goes into the final state, then A |+| B will go into the first state of B *)
lemma tm_comp_next: 
  assumes a_ht: "steps0 (1, tp) A n = (0, tp')"
    and a_wf: "tm_wf (A, 0)"
  obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"
proof -
  assume a: "⋀n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') ⟹ thesis"
  obtain stp' where fin: "¬ is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')"
    using before_final[OF a_ht] by blast
  from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'"
    by (rule tm_comp_steps)
  from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')"
    by (simp only: step_red)

  have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" 
    by (simp only: step_red)
  also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp
  also have "... = (Suc (length A div 2), tp')" 
    by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]])
  finally show thesis using a by blast
qed

lemma tm_comp_fetch_second_zero:
  assumes h1: "fetch B s x = (a, 0)"
    and hs: "tm_wf (A, 0)" "s ≠ 0"
  shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)"
  using h1 hs
  by(cases x; cases s; fastforce simp: tm_comp_length nth_append)

lemma tm_comp_fetch_second_inst:
  assumes h1: "fetch B sa x = (a, s)"
    and hs: "tm_wf (A, 0)" "sa ≠ 0" "s ≠ 0"
  shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
  using h1 hs
  by(cases x; cases sa; fastforce simp: tm_comp_length nth_append)


lemma tm_comp_second:
  assumes a_wf: "tm_wf (A, 0)"
    and steps: "steps0 (1, l, r) B stp = (s', l', r')"
  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp 
    = (if s' = 0 then 0 else s' + length A div 2, l', r')"
  using steps
proof(induct stp arbitrary: s' l' r')
  case 0
  then show ?case by simp
next
  case (Suc stp s' l' r')
  obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')"
    by (metis is_final.cases)
  then have ih1: "s'' = 0 ⟹ steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')"
    and ih2: "s'' ≠ 0 ⟹ steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')"
    using Suc by (auto)
  have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact

  { assume "s'' = 0"
    then have ?case using a h ih1 by (simp del: steps.simps) 
  } moreover
  { assume as: "s'' ≠ 0" "s' = 0"
    from as a h 
    have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps)
    with as have ?case
      apply(cases "fetch B s'' (read r'')")
      by (auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] ih2[OF as(1)]
          simp del: tm_comp.simps steps.simps)
  } moreover
  { assume as: "s'' ≠ 0" "s' ≠ 0"
    from as a h
    have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps)
    with as have ?case
      apply(simp add: ih2[OF as(1)] del: tm_comp.simps steps.simps)
      apply(case_tac "fetch B s'' (read r'')")
      apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps)
      done
  }
  ultimately show ?case by blast
qed


lemma tm_comp_final:
  assumes "tm_wf (A, 0)"  
    and "steps0 (1, l, r) B stp = (0, l', r')"
  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp = (0, l', r')"
  using tm_comp_second[OF assms] by (simp)

end

(* Title: thys/Turing_Hoare.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Hoare Rules for TMs›

theory Turing_Hoare
  imports Turing
begin


type_synonym assert = "tape ⇒ bool"

definition 
  assert_imp :: "assert ⇒ assert ⇒ bool" ("_ ↦ _" [0, 0] 100)
  where
    "P ↦ Q ≡ ∀l r. P (l, r) ⟶ Q (l, r)"

lemma refl_assert[intro, simp]:
  "P ↦ P"
  unfolding assert_imp_def by simp

fun 
  holds_for :: "(tape ⇒ bool) ⇒ config ⇒ bool" ("_ holds'_for _" [100, 99] 100)
  where
    "P holds_for (s, l, r) = P (l, r)"  

lemma is_final_holds[simp]:
  assumes "is_final c"
  shows "Q holds_for (steps c p n) = Q holds_for c"
  using assms 
  by(induct n;cases c,auto)

(* Hoare Rules *)

(* halting case *)
definition
  Hoare_halt :: "assert ⇒ tprog0 ⇒ assert ⇒ bool" ("({(1_)}/ (_)/ {(1_)})" 50)
  where
    "{P} p {Q} ≡ (∀tp. P tp ⟶ (∃n. is_final (steps0 (1, tp) p n) ∧ Q holds_for (steps0 (1, tp) p n)))"

(* not halting case *)
definition
  Hoare_unhalt :: "assert ⇒ tprog0 ⇒ bool" ("({(1_)}/ (_)) ↑" 50)
  where
    "{P} p ↑ ≡ ∀tp. P tp ⟶ (∀ n . ¬ (is_final (steps0 (1, tp) p n)))"


lemma Hoare_haltI:
  assumes "⋀l r. P (l, r) ⟹ ∃n. is_final (steps0 (1, (l, r)) p n) ∧ Q holds_for (steps0 (1, (l, r)) p n)"
  shows "{P} p {Q}"
  unfolding Hoare_halt_def 
  using assms by auto

lemma Hoare_unhaltI:
  assumes "⋀l r n. P (l, r) ⟹ ¬ is_final (steps0 (1, (l, r)) p n)"
  shows "{P} p ↑"
  unfolding Hoare_unhalt_def 
  using assms by auto




text ‹
  {P} A {Q}   {Q} B {S}  A well-formed
  -----------------------------------------
  {P} A |+| B {S}
›


lemma Hoare_plus_halt [case_names A_halt B_halt A_wf]: 
  assumes A_halt : "{P} A {Q}"
    and B_halt : "{Q} B {S}"
    and A_wf : "tm_wf (A, 0)"
  shows "{P} A |+| B {S}"
proof(rule Hoare_haltI)
  fix l r
  assume h: "P (l, r)"
  then obtain n1 l' r' 
    where "is_final (steps0 (1, l, r) A n1)"  
      and a1: "Q holds_for (steps0 (1, l, r) A n1)"
      and a2: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def
    by (metis is_final_eq surj_pair) 
  then obtain n2 
    where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_wf by (rule_tac tm_comp_next) 
  moreover
  from a1 a2 have "Q (l', r')" by (simp)
  then obtain n3 l'' r''
    where "is_final (steps0 (1, l', r') B n3)" 
      and b1: "S holds_for (steps0 (1, l', r') B n3)"
      and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')"
    using B_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
    using A_wf by (rule_tac tm_comp_final) 
  ultimately show 
    "∃n. is_final (steps0 (1, l, r) (A |+| B) n) ∧ S holds_for (steps0 (1, l, r) (A |+| B) n)"
    using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
qed

text ‹
  {P} A {Q}   {Q} B loops   A well-formed
  ------------------------------------------
          {P} A |+| B  loops
›

lemma Hoare_plus_unhalt [case_names A_halt B_unhalt A_wf]:
  assumes A_halt: "{P} A {Q}"
    and B_uhalt: "{Q} B ↑"
    and A_wf : "tm_wf (A, 0)"
  shows "{P} (A |+| B) ↑"
proof(rule_tac Hoare_unhaltI)
  fix n l r 
  assume h: "P (l, r)"
  then obtain n1 l' r'
    where a: "is_final (steps0 (1, l, r) A n1)" 
      and b: "Q holds_for (steps0 (1, l, r) A n1)"
      and c: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_wf by (rule_tac tm_comp_next)
  then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
  proof(cases "n2 ≤ n")
    case True
    from b c have "Q (l', r')" by simp
    then have "∀ n. ¬ is_final (steps0 (1, l', r') B n)  "
      using B_uhalt unfolding Hoare_unhalt_def by simp
    then have "¬ is_final (steps0 (1, l', r') B (n - n2))" by auto
    then obtain s'' l'' r'' 
      where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" 
        and "¬ is_final (s'', l'', r'')" by (metis surj_pair)
    then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
      using A_wf by (auto dest: tm_comp_second simp del: tm_wf.simps)
    then have "¬ is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
      using A_wf by (simp only: steps_add eq) simp
    then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)" 
      using ‹n2 ≤ n› by simp
  next 
    case False
    then obtain n3 where "n = n2 - n3"
      using diff_le_self le_imp_diff_is_add nat_le_linear
        add.commute by metis
    moreover
    with eq show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
      by (simp add: not_is_final[where ?n1.0="n2"])
  qed
qed

lemma Hoare_consequence:
  assumes "P' ↦ P" "{P} p {Q}" "Q ↦ Q'"
  shows "{P'} p {Q'}"
  using assms
  unfolding Hoare_halt_def assert_imp_def
  by (metis holds_for.simps surj_pair)



end

(* Title: thys/Uncomputable.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
*)

chapter ‹Undeciablity of the Halting Problem›

theory Uncomputable
  imports Turing_Hoare
begin

lemma numeral:
  shows "2 = Suc 1"
    and "3 = Suc 2"
    and "4 = Suc 3" 
    and "5 = Suc 4" 
    and "6 = Suc 5" 
    and "7 = Suc 6"
    and "8 = Suc 7" 
    and "9 = Suc 8" 
    and "10 = Suc 9"
    and "11 = Suc 10"
    and "12 = Suc 11"
  by simp_all

lemma gr1_conv_Suc:"Suc 0 < mr ⟷ (∃ nat. mr = Suc (Suc nat))" by presburger

text ‹The Copying TM, which duplicates its input.›

definition 
  tcopy_begin :: "instr list"
  where
    "tcopy_begin ≡ [(W0, 0), (R, 2), (R, 3), (R, 2),
                 (W1, 3), (L, 4), (L, 4), (L, 0)]"

definition 
  tcopy_loop :: "instr list"
  where
    "tcopy_loop ≡ [(R, 0), (R, 2),  (R, 3), (W0, 2),
                 (R, 3), (R, 4), (W1, 5), (R, 4),
                 (L, 6), (L, 5), (L, 6), (L, 1)]"

definition 
  tcopy_end :: "instr list"
  where
    "tcopy_end ≡ [(L, 0), (R, 2), (W1, 3), (L, 4),
                (R, 2), (R, 2), (L, 5), (W0, 4),
                (R, 0), (L, 5)]"

definition 
  tcopy :: "instr list"
  where
    "tcopy ≡ (tcopy_begin |+| tcopy_loop) |+| tcopy_end"


(* tcopy_begin *)

fun 
  inv_begin0 :: "nat ⇒ tape ⇒ bool" and
  inv_begin1 :: "nat ⇒ tape ⇒ bool" and
  inv_begin2 :: "nat ⇒ tape ⇒ bool" and
  inv_begin3 :: "nat ⇒ tape ⇒ bool" and
  inv_begin4 :: "nat ⇒ tape ⇒ bool"
  where
    "inv_begin0 n (l, r) = ((n > 1 ∧ (l, r) = (Oc ↑ (n - 2), [Oc, Oc, Bk, Oc])) ∨   
                          (n = 1 ∧ (l, r) = ([], [Bk, Oc, Bk, Oc])))"
  | "inv_begin1 n (l, r) = ((l, r) = ([], Oc ↑ n))"
  | "inv_begin2 n (l, r) = (∃ i j. i > 0 ∧ i + j = n ∧ (l, r) = (Oc ↑ i, Oc ↑ j))"
  | "inv_begin3 n (l, r) = (n > 0 ∧ (l, tl r) = (Bk # Oc ↑ n, []))"
  | "inv_begin4 n (l, r) = (n > 0 ∧ (l, r) = (Oc ↑ n, [Bk, Oc]) ∨ (l, r) = (Oc ↑ (n - 1), [Oc, Bk, Oc]))"

fun inv_begin :: "nat ⇒ config ⇒ bool"
  where
    "inv_begin n (s, tp) = 
        (if s = 0 then inv_begin0 n tp else
         if s = 1 then inv_begin1 n tp else
         if s = 2 then inv_begin2 n tp else
         if s = 3 then inv_begin3 n tp else
         if s = 4 then inv_begin4 n tp 
         else False)"

lemma split_head_repeat[simp]:
  "Oc # list1 = Bk ↑ j @ list2 ⟷ j = 0 ∧ Oc # list1 = list2"
  "Bk # list1 = Oc ↑ j @ list2 ⟷ j = 0 ∧ Bk # list1 = list2"
  "Bk ↑ j @ list2 = Oc # list1 ⟷ j = 0 ∧ Oc # list1 = list2"
  "Oc ↑ j @ list2 = Bk # list1 ⟷ j = 0 ∧ Bk # list1 = list2"
  by(cases j;force)+

lemma inv_begin_step_E: "⟦0 < i; 0 < j⟧ ⟹ 
  ∃ia>0. ia + j - Suc 0 = i + j ∧ Oc # Oc ↑ i = Oc ↑ ia"
  by (rule_tac x = "Suc i" in exI, simp)

lemma inv_begin_step: 
  assumes "inv_begin n cf"
    and "n > 0"
  shows "inv_begin n (step0 cf tcopy_begin)"
  using assms
  unfolding tcopy_begin_def
  apply(cases cf)
  apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
  apply(cases "hd (snd (snd cf))";cases "(snd (snd cf))",auto)
  done

lemma inv_begin_steps: 
  assumes "inv_begin n cf"
    and "n > 0"
  shows "inv_begin n (steps0 cf tcopy_begin stp)"
  apply(induct stp)
   apply(simp add: assms)
  apply(auto simp del: steps.simps)
  apply(rule_tac inv_begin_step)
   apply(simp_all add: assms)
  done

lemma begin_partial_correctness:
  assumes "is_final (steps0 (1, [], Oc ↑ n) tcopy_begin stp)"
  shows "0 < n ⟹ {inv_begin1 n} tcopy_begin {inv_begin0 n}"
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n" "inv_begin1 n (l, r)"
  have "inv_begin n (steps0 (1, [], Oc ↑ n) tcopy_begin stp)"
    using h by (rule_tac inv_begin_steps) (simp_all)
  then show
    "∃stp. is_final (steps0 (1, l, r) tcopy_begin stp) ∧ 
    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
    using h assms
    apply(rule_tac x = stp in exI)
    apply(case_tac "(steps0 (1, [], Oc ↑ n) tcopy_begin stp)", simp)
    done
qed

fun measure_begin_state :: "config ⇒ nat"
  where
    "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"

fun measure_begin_step :: "config ⇒ nat"
  where
    "measure_begin_step (s, l, r) = 
        (if s = 2 then length r else
         if s = 3 then (if r = [] ∨ r = [Bk] then 1 else 0) else
         if s = 4 then length l 
         else 0)"

definition
  "measure_begin = measures [measure_begin_state, measure_begin_step]"

lemma wf_measure_begin:
  shows "wf measure_begin" 
  unfolding measure_begin_def 
  by auto

lemma measure_begin_induct [case_names Step]: 
  "⟦⋀n. ¬ P (f n) ⟹ (f (Suc n), (f n)) ∈ measure_begin⟧ ⟹ ∃n. P (f n)"
  using wf_measure_begin
  by (metis wf_iff_no_infinite_down_chain)

lemma begin_halts: 
  assumes h: "x > 0"
  shows "∃ stp. is_final (steps0 (1, [], Oc ↑ x) tcopy_begin stp)"
proof (induct rule: measure_begin_induct) 
  case (Step n)
  have "¬ is_final (steps0 (1, [], Oc ↑ x) tcopy_begin n)" by fact
  moreover
  have "inv_begin x (steps0 (1, [], Oc ↑ x) tcopy_begin n)"
    by (rule_tac inv_begin_steps) (simp_all add:  h)
  moreover
  obtain s l r where eq: "(steps0 (1, [], Oc ↑ x) tcopy_begin n) = (s, l, r)"
    by (metis measure_begin_state.cases)
  ultimately 
  have "(step0 (s, l, r) tcopy_begin, s, l, r) ∈ measure_begin"
    apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
    apply(subgoal_tac "r = [Oc]")
     apply(auto)
    by (metis cell.exhaust list.exhaust list.sel(3))
  then 
  show "(steps0 (1, [], Oc ↑ x) tcopy_begin (Suc n), steps0 (1, [], Oc ↑ x) tcopy_begin n) ∈ measure_begin"
    using eq by (simp only: step_red)
qed

lemma begin_correct: 
  shows "0 < n ⟹ {inv_begin1 n} tcopy_begin {inv_begin0 n}"
  using begin_partial_correctness begin_halts by blast

declare tm_comp.simps [simp del] 
declare adjust.simps[simp del] 
declare shift.simps[simp del]
declare tm_wf.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]

(* tcopy_loop *)

fun 
  inv_loop1_loop :: "nat ⇒ tape ⇒ bool" and
  inv_loop1_exit :: "nat ⇒ tape ⇒ bool" and
  inv_loop5_loop :: "nat ⇒ tape ⇒ bool" and
  inv_loop5_exit :: "nat ⇒ tape ⇒ bool" and
  inv_loop6_loop :: "nat ⇒ tape ⇒ bool" and
  inv_loop6_exit :: "nat ⇒ tape ⇒ bool"
  where
    "inv_loop1_loop n (l, r) = (∃ i j. i + j + 1 = n ∧ (l, r) = (Oc↑i, Oc#Oc#Bk↑j @ Oc↑j) ∧ j > 0)"
  | "inv_loop1_exit n (l, r) = (0 < n ∧ (l, r) = ([], Bk#Oc#Bk↑n @ Oc↑n))"
  | "inv_loop5_loop x (l, r) = 
     (∃ i j k t. i + j = Suc x ∧ i > 0 ∧ j > 0 ∧ k + t = j ∧ t > 0 ∧ (l, r) = (Oc↑k@Bk↑j@Oc↑i, Oc↑t))"
  | "inv_loop5_exit x (l, r) = 
     (∃ i j. i + j = Suc x ∧ i > 0 ∧ j > 0 ∧ (l, r) = (Bk↑(j - 1)@Oc↑i, Bk # Oc↑j))"
  | "inv_loop6_loop x (l, r) = 
     (∃ i j k t. i + j = Suc x ∧ i > 0 ∧ k + t + 1 = j ∧ (l, r) = (Bk↑k @ Oc↑i, Bk↑(Suc t) @ Oc↑j))"
  | "inv_loop6_exit x (l, r) = 
     (∃ i j. i + j = x ∧ j > 0 ∧ (l, r) = (Oc↑i, Oc#Bk↑j @ Oc↑j))"

fun 
  inv_loop0 :: "nat ⇒ tape ⇒ bool" and
  inv_loop1 :: "nat ⇒ tape ⇒ bool" and
  inv_loop2 :: "nat ⇒ tape ⇒ bool" and
  inv_loop3 :: "nat ⇒ tape ⇒ bool" and
  inv_loop4 :: "nat ⇒ tape ⇒ bool" and
  inv_loop5 :: "nat ⇒ tape ⇒ bool" and
  inv_loop6 :: "nat ⇒ tape ⇒ bool"
  where
    "inv_loop0 n (l, r) =  (0 < n ∧ (l, r) = ([Bk], Oc # Bk↑n @ Oc↑n))"
  | "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r) ∨ inv_loop1_exit n (l, r))"
  | "inv_loop2 n (l, r) = (∃ i j any. i + j = n ∧ n > 0 ∧ i > 0 ∧ j > 0 ∧ (l, r) = (Oc↑i, any#Bk↑j@Oc↑j))"
  | "inv_loop3 n (l, r) = 
     (∃ i j k t. i + j = n ∧ i > 0 ∧ j > 0 ∧  k + t = Suc j ∧ (l, r) = (Bk↑k@Oc↑i, Bk↑t@Oc↑j))"
  | "inv_loop4 n (l, r) = 
     (∃ i j k t. i + j = n ∧ i > 0 ∧ j > 0 ∧  k + t = j ∧ (l, r) = (Oc↑k @ Bk↑(Suc j)@Oc↑i, Oc↑t))"
  | "inv_loop5 n (l, r) = (inv_loop5_loop n (l, r) ∨ inv_loop5_exit n (l, r))"
  | "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r) ∨ inv_loop6_exit n (l, r))"

fun inv_loop :: "nat ⇒ config ⇒ bool"
  where
    "inv_loop x (s, l, r) = 
         (if s = 0 then inv_loop0 x (l, r)
          else if s = 1 then inv_loop1 x (l, r)
          else if s = 2 then inv_loop2 x (l, r)
          else if s = 3 then inv_loop3 x (l, r)
          else if s = 4 then inv_loop4 x (l, r)
          else if s = 5 then inv_loop5 x (l, r)
          else if s = 6 then inv_loop6 x (l, r)
          else False)"

declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
  inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
  inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
  inv_loop6.simps[simp del]

lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc ↑ t ⟹ RR"
  by (cases t, auto)

lemma inv_loop3_Bk_empty_via_2[elim]: "⟦0 < x; inv_loop2 x (b, [])⟧ ⟹ inv_loop3 x (Bk # b, [])"
  by (auto simp: inv_loop2.simps inv_loop3.simps)

lemma inv_loop3_Bk_empty[elim]: "⟦0 < x; inv_loop3 x (b, [])⟧ ⟹ inv_loop3 x (Bk # b, [])"
  by (auto simp: inv_loop3.simps)

lemma inv_loop5_Oc_empty_via_4[elim]: "⟦0 < x; inv_loop4 x (b, [])⟧ ⟹ inv_loop5 x (b, [Oc])"
  by(auto simp: inv_loop4.simps inv_loop5.simps;force)

lemma inv_loop1_Bk[elim]: "⟦0 < x; inv_loop1 x (b, Bk # list)⟧ ⟹ list = Oc # Bk ↑ x @ Oc ↑ x"
  by (auto simp: inv_loop1.simps)

lemma inv_loop3_Bk_via_2[elim]: "⟦0 < x; inv_loop2 x (b, Bk # list)⟧ ⟹ inv_loop3 x (Bk # b, list)"
  by(auto simp: inv_loop2.simps inv_loop3.simps;force)

lemma inv_loop3_Bk_move[elim]: "⟦0 < x; inv_loop3 x (b, Bk # list)⟧ ⟹ inv_loop3 x (Bk # b, list)"
  apply(auto simp: inv_loop3.simps)
   apply (rename_tac i j k t)
   apply(rule_tac [!] x = i in exI, 
      rule_tac [!] x = j in exI, simp_all)
   apply(case_tac [!] t, auto)
  done

lemma inv_loop5_Oc_via_4_Bk[elim]: "⟦0 < x; inv_loop4 x (b, Bk # list)⟧ ⟹ inv_loop5 x (b, Oc # list)"
  by (auto simp: inv_loop4.simps inv_loop5.simps)

lemma inv_loop6_Bk_via_5[elim]: "⟦0 < x; inv_loop5 x ([], Bk # list)⟧ ⟹ inv_loop6 x ([], Bk # Bk # list)"
  by (auto simp: inv_loop6.simps inv_loop5.simps)

lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
  by (auto simp: inv_loop5.simps)

lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
  by (auto simp: inv_loop6.simps)

declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
  inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]

lemma inv_loop6_loopBk_via_5[elim]:"⟦0 < x; inv_loop5_exit x (b, Bk # list); b ≠ []; hd b = Bk⟧ 
          ⟹ inv_loop6_loop x (tl b, Bk # Bk # list)"
  apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
  apply(erule_tac exE)+
  apply(rename_tac i j)
  apply(rule_tac x = i in exI, 
      rule_tac x = j in exI,
      rule_tac x = "j - Suc (Suc 0)" in exI, 
      rule_tac x = "Suc 0" in exI, auto)
   apply(case_tac [!] j, simp_all)
   apply(case_tac [!] "j-1", simp_all)
  done

lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
  by (auto simp: inv_loop6_loop.simps)

lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "⟦x > 0; inv_loop5_exit x (b, Bk # list); b ≠ []; hd b = Oc⟧ ⟹ 
  inv_loop6_exit x (tl b, Oc # Bk # list)"
  apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
  apply(erule_tac exE)+
  apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
  apply(rename_tac i j)
  apply(case_tac j;case_tac "j-1", auto)
  done

lemma inv_loop6_Bk_tail_via_5[elim]: "⟦0 < x; inv_loop5 x (b, Bk # list); b ≠ []⟧ ⟹ inv_loop6 x (tl b, hd b # Bk # list)"
  apply(simp add: inv_loop5.simps inv_loop6.simps)
  apply(cases "hd b", simp_all, auto)
  done

lemma inv_loop6_loop_Bk_Bk_drop[elim]: "⟦0 < x; inv_loop6_loop x (b, Bk # list); b ≠ []; hd b = Bk⟧
              ⟹ inv_loop6_loop x (tl b, Bk # Bk # list)"
  apply(simp only: inv_loop6_loop.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI, rule_tac x = j in exI, 
      rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
   apply(case_tac [!] k, auto)
  done

lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "⟦0 < x; inv_loop6_loop x (b, Bk # list); b ≠ []; hd b = Oc⟧ 
        ⟹ inv_loop6_exit x (tl b, Oc # Bk # list)"
  apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
   apply(case_tac [!] k, auto)
  done

lemma inv_loop6_Bk_tail[elim]: "⟦0 < x; inv_loop6 x (b, Bk # list); b ≠ []⟧ ⟹ inv_loop6 x (tl b, hd b # Bk # list)"
  apply(simp add: inv_loop6.simps)
  apply(case_tac "hd b", simp_all, auto)
  done

lemma inv_loop2_Oc_via_1[elim]: "⟦0 < x; inv_loop1 x (b, Oc # list)⟧ ⟹ inv_loop2 x (Oc # b, list)"
  apply(auto simp: inv_loop1.simps inv_loop2.simps,force)
  done

lemma inv_loop2_Bk_via_Oc[elim]: "⟦0 < x; inv_loop2 x (b, Oc # list)⟧ ⟹ inv_loop2 x (b, Bk # list)"
  by (auto simp: inv_loop2.simps)

lemma inv_loop4_Oc_via_3[elim]: "⟦0 < x; inv_loop3 x (b, Oc # list)⟧ ⟹ inv_loop4 x (Oc # b, list)"
  apply(auto simp: inv_loop3.simps inv_loop4.simps)
   apply(rename_tac i j)
   apply(rule_tac [!] x = i in exI, auto)
   apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI)
   apply(case_tac [!] j, auto)
  done

lemma inv_loop4_Oc_move[elim]:
  assumes "0 < x" "inv_loop4 x (b, Oc # list)"
  shows "inv_loop4 x (Oc # b, list)"
proof -
  from assms[unfolded inv_loop4.simps] obtain i j k t where
    "i + j = x"
    "0 < i" "0 < j" "k + t = j" "(b, Oc # list) = (Oc ↑ k @ Bk ↑ Suc j @ Oc ↑ i, Oc ↑ t)"
    by auto  
  thus ?thesis unfolding inv_loop4.simps
    apply(rule_tac [!] x = "i" in exI,rule_tac [!] x = "j" in exI)
    apply(rule_tac [!] x = "Suc k" in exI,rule_tac [!] x = "t - 1" in exI)
    by(cases t,auto)
qed

lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
  by (auto simp: inv_loop5_exit.simps)

lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " ⟦inv_loop5_loop x (b, Oc # list); b ≠ []; hd b = Bk⟧
  ⟹ inv_loop5_exit x (tl b, Bk # Oc # list)"
  apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI)
  apply(case_tac k, auto)
  done

lemma inv_loop5_loop_Oc_Oc_drop[elim]: "⟦inv_loop5_loop x (b, Oc # list); b ≠ []; hd b = Oc⟧ 
           ⟹ inv_loop5_loop x (tl b, Oc # Oc # list)"
  apply(simp only:  inv_loop5_loop.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j k t)
  apply(rule_tac x = i in exI, rule_tac x = j in exI)
  apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI)
  apply(case_tac k, auto)
  done

lemma inv_loop5_Oc_tl[elim]: "⟦inv_loop5 x (b, Oc # list); b ≠ []⟧ ⟹ inv_loop5 x (tl b, hd b # Oc # list)"
  apply(simp add: inv_loop5.simps)
  apply(cases "hd b", simp_all, auto)
  done

lemma inv_loop1_Bk_Oc_via_6[elim]: "⟦0 < x; inv_loop6 x ([], Oc # list)⟧ ⟹ inv_loop1 x ([], Bk # Oc # list)"
  by(auto simp: inv_loop6.simps inv_loop1.simps inv_loop6_loop.simps inv_loop6_exit.simps)

lemma inv_loop1_Oc_via_6[elim]: "⟦0 < x; inv_loop6 x (b, Oc # list); b ≠ []⟧ 
           ⟹ inv_loop1 x (tl b, hd b # Oc # list)"
  by(auto simp: inv_loop6.simps inv_loop1.simps inv_loop6_loop.simps inv_loop6_exit.simps)


lemma inv_loop_nonempty[simp]:
  "inv_loop1 x (b, []) = False"
  "inv_loop2 x ([], b) = False"
  "inv_loop2 x (l', []) = False"
  "inv_loop3 x (b, []) = False"
  "inv_loop4 x ([], b) = False"
  "inv_loop5 x ([], list) = False"
  "inv_loop6 x ([], Bk # xs) = False"
  by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps 
      inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
      inv_loop6_loop.simps)

lemma inv_loop_nonemptyE[elim]:
  "⟦inv_loop5 x (b, [])⟧ ⟹ RR" "inv_loop6 x (b, []) ⟹ RR" 
  "⟦inv_loop1 x (b, Bk # list)⟧ ⟹ b = []"
  by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
      inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)

lemma inv_loop6_Bk_Bk_drop[elim]: "⟦inv_loop6 x ([], Bk # list)⟧ ⟹ inv_loop6 x ([], Bk # Bk # list)"
  by (simp)

lemma inv_loop_step: 
  "⟦inv_loop x cf; x > 0⟧ ⟹ inv_loop x (step cf (tcopy_loop, 0))"
  apply(cases cf, cases "snd (snd cf)"; cases "hd (snd (snd cf))")
     apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
  done

lemma inv_loop_steps:
  "⟦inv_loop x cf; x > 0⟧ ⟹ inv_loop x (steps cf (tcopy_loop, 0) stp)"
  apply(induct stp, simp add: steps.simps, simp)
  apply(erule_tac inv_loop_step, simp)
  done

fun loop_stage :: "config ⇒ nat"
  where
    "loop_stage (s, l, r) = (if s = 0 then 0
                           else (Suc (length (takeWhile (λa. a = Oc) (rev l @ r)))))"

fun loop_state :: "config ⇒ nat"
  where
    "loop_state (s, l, r) = (if s = 2 ∧ hd r = Oc then 0
                           else if s = 1 then 1
                           else 10 - s)"

fun loop_step :: "config ⇒ nat"
  where
    "loop_step (s, l, r) = (if s = 3 then length r
                          else if s = 4 then length r
                          else if s = 5 then length l 
                          else if s = 6 then length l
                          else 0)"

definition measure_loop :: "(config × config) set"
  where
    "measure_loop = measures [loop_stage, loop_state, loop_step]"

lemma wf_measure_loop: "wf measure_loop"
  unfolding measure_loop_def
  by (auto)

lemma measure_loop_induct [case_names Step]: 
  "⟦⋀n. ¬ P (f n) ⟹ (f (Suc n), (f n)) ∈ measure_loop⟧ ⟹ ∃n. P (f n)"
  using wf_measure_loop
  by (metis wf_iff_no_infinite_down_chain)

lemma inv_loop4_not_just_Oc[elim]: 
  "⟦inv_loop4 x (l', []);
  length (takeWhile (λa. a = Oc) (rev l' @ [Oc])) ≠ 
  length (takeWhile (λa. a = Oc) (rev l'))⟧
  ⟹ RR"
  "⟦inv_loop4 x (l', Bk # list);
   length (takeWhile (λa. a = Oc) (rev l' @ Oc # list)) ≠ 
    length (takeWhile (λa. a = Oc) (rev l' @ Bk # list))⟧
    ⟹ RR"
   apply(auto simp: inv_loop4.simps)
  apply(rename_tac i j)
  apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
  done

lemma takeWhile_replicate_append: 
  "P a ⟹ takeWhile P (a↑x @ ys) = a↑x @ takeWhile P ys"
  by (induct x, auto)

lemma takeWhile_replicate: 
  "P a ⟹ takeWhile P (a↑x) = a↑x"
  by (induct x, auto)

lemma inv_loop5_Bk_E[elim]: 
  "⟦inv_loop5 x (l', Bk # list); l' ≠ []; 
   length (takeWhile (λa. a = Oc) (rev (tl l') @ hd l' # Bk # list)) ≠
   length (takeWhile (λa. a = Oc) (rev l' @ Bk # list))⟧
   ⟹ RR"
  apply(cases "length list";cases "length list - 1"
      ,auto simp: inv_loop5.simps inv_loop5_exit.simps
      takeWhile_replicate_append takeWhile_replicate)
   apply(cases "length list - 2"; force simp add: List.takeWhile_tail)+
  done

lemma inv_loop1_hd_Oc[elim]: "⟦inv_loop1 x (l', Oc # list)⟧ ⟹ hd list = Oc"
  by (auto simp: inv_loop1.simps)

lemma inv_loop6_not_just_Bk[dest!]: 
  "⟦length (takeWhile P (rev (tl l') @ hd l' # list)) ≠ 
  length (takeWhile P (rev l' @ list))⟧
  ⟹ l' = []"
  apply(cases l', simp_all)
  done

lemma inv_loop2_OcE[elim]:
  "⟦inv_loop2 x (l', Oc # list); l' ≠ []⟧ ⟹ 
  length (takeWhile (λa. a = Oc) (rev l' @ Bk # list)) <
  length (takeWhile (λa. a = Oc) (rev l' @ Oc # list))"
  apply(auto simp: inv_loop2.simps takeWhile_tail takeWhile_replicate_append
      takeWhile_replicate)
  done

lemma loop_halts: 
  assumes h: "n > 0" "inv_loop n (1, l, r)"
  shows "∃ stp. is_final (steps0 (1, l, r) tcopy_loop stp)"
proof (induct rule: measure_loop_induct) 
  case (Step stp)
  have "¬ is_final (steps0 (1, l, r) tcopy_loop stp)" by fact
  moreover
  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
    by (rule_tac inv_loop_steps) (simp_all only: h)
  moreover
  obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"
    by (metis measure_begin_state.cases)
  ultimately 
  have "(step0 (s, l', r') tcopy_loop, s, l', r') ∈ measure_loop"
    using h(1)
    apply(cases r';cases "hd r'")
       apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)
    done
  then 
  show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) ∈ measure_loop"
    using eq by (simp only: step_red)
qed

lemma loop_correct:
  assumes "0 < n"
  shows "{inv_loop1 n} tcopy_loop {inv_loop0 n}"
  using assms
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n" "inv_loop1 n (l, r)"
  then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)" 
    using loop_halts
    apply(simp add: inv_loop.simps)
    apply(blast)
    done
  moreover
  have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
    using h 
    by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)
  ultimately show
    "∃stp. is_final (steps0 (1, l, r) tcopy_loop stp) ∧ 
    inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"
    using h(1) 
    apply(rule_tac x = stp in exI)
    apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")
    apply(simp add: inv_loop.simps)
    done
qed




(* tcopy_end *)

fun
  inv_end5_loop :: "nat ⇒ tape ⇒ bool" and
  inv_end5_exit :: "nat ⇒ tape ⇒ bool" 
  where  
    "inv_end5_loop x (l, r) = 
     (∃ i j. i + j = x ∧ x > 0 ∧ j > 0 ∧ l = Oc↑i @ [Bk] ∧ r = Oc↑j @ Bk # Oc↑x)"
  | "inv_end5_exit x (l, r) = (x > 0 ∧ l = [] ∧ r = Bk # Oc↑x @ Bk # Oc↑x)"

fun 
  inv_end0 :: "nat ⇒ tape ⇒  bool" and
  inv_end1 :: "nat ⇒ tape ⇒ bool" and
  inv_end2 :: "nat ⇒ tape ⇒ bool" and
  inv_end3 :: "nat ⇒ tape ⇒ bool" and
  inv_end4 :: "nat ⇒ tape ⇒ bool" and 
  inv_end5 :: "nat ⇒ tape ⇒ bool" 
  where
    "inv_end0 n (l, r) = (n > 0 ∧ (l, r) = ([Bk], Oc↑n @ Bk # Oc↑n))"
  | "inv_end1 n (l, r) = (n > 0 ∧ (l, r) = ([Bk], Oc # Bk↑n @ Oc↑n))"
  | "inv_end2 n (l, r) = (∃ i j. i + j = Suc n ∧ n > 0 ∧ l = Oc↑i @ [Bk] ∧ r = Bk↑j @ Oc↑n)"
  | "inv_end3 n (l, r) =
     (∃ i j. n > 0 ∧ i + j = n ∧ l = Oc↑i @ [Bk] ∧ r = Oc # Bk↑j@ Oc↑n)"
  | "inv_end4 n (l, r) = (∃ any. n > 0 ∧ l = Oc↑n @ [Bk] ∧ r = any#Oc↑n)"
  | "inv_end5 n (l, r) = (inv_end5_loop n (l, r) ∨ inv_end5_exit n (l, r))"

fun 
  inv_end :: "nat ⇒ config ⇒ bool"
  where
    "inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)
                          else if s = 1 then inv_end1 n (l, r)
                          else if s = 2 then inv_end2 n (l, r)
                          else if s = 3 then inv_end3 n (l, r)
                          else if s = 4 then inv_end4 n (l, r)
                          else if s = 5 then inv_end5 n (l, r)
                          else False)"

declare inv_end.simps[simp del] inv_end1.simps[simp del]
  inv_end0.simps[simp del] inv_end2.simps[simp del]
  inv_end3.simps[simp del] inv_end4.simps[simp del]
  inv_end5.simps[simp del]

lemma inv_end_nonempty[simp]:
  "inv_end1 x (b, []) = False"
  "inv_end1 x ([], list) = False"
  "inv_end2 x (b, []) = False"
  "inv_end3 x (b, []) = False"
  "inv_end4 x (b, []) = False"
  "inv_end5 x (b, []) = False"
  "inv_end5 x ([], Oc # list) = False"
  by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)

lemma inv_end0_Bk_via_1[elim]: "⟦0 < x; inv_end1 x (b, Bk # list); b ≠ []⟧
  ⟹ inv_end0 x (tl b, hd b # Bk # list)"
  by (auto simp: inv_end1.simps inv_end0.simps)

lemma inv_end3_Oc_via_2[elim]: "⟦0 < x; inv_end2 x (b, Bk # list)⟧ 
  ⟹ inv_end3 x (b, Oc # list)"
  apply(auto simp: inv_end2.simps inv_end3.simps)
  by (metis Cons_replicate_eq One_nat_def Suc_inject Suc_pred add_Suc_right cell.distinct(1)
      empty_replicate list.sel(3) neq0_conv self_append_conv2 tl_append2 tl_replicate)

lemma inv_end2_Bk_via_3[elim]: "⟦0 < x; inv_end3 x (b, Bk # list)⟧ ⟹ inv_end2 x (Bk # b, list)"
  by (auto simp: inv_end2.simps inv_end3.simps)

lemma inv_end5_Bk_via_4[elim]: "⟦0 < x; inv_end4 x ([], Bk # list)⟧ ⟹ 
  inv_end5 x ([], Bk # Bk # list)"
  by (auto simp: inv_end4.simps inv_end5.simps)

lemma inv_end5_Bk_tail_via_4[elim]: "⟦0 < x; inv_end4 x (b, Bk # list); b ≠ []⟧ ⟹ 
  inv_end5 x (tl b, hd b # Bk # list)"
  apply(auto simp: inv_end4.simps inv_end5.simps)
  apply(rule_tac x = 1 in exI, simp)
  done

lemma inv_end0_Bk_via_5[elim]: "⟦0 < x; inv_end5 x (b, Bk # list)⟧ ⟹ inv_end0 x (Bk # b, list)"
  by(auto simp: inv_end5.simps inv_end0.simps gr0_conv_Suc)

lemma inv_end2_Oc_via_1[elim]: "⟦0 < x; inv_end1 x (b, Oc # list)⟧ ⟹ inv_end2 x (Oc # b, list)"
  by (auto simp: inv_end1.simps inv_end2.simps)

lemma inv_end4_Bk_Oc_via_2[elim]: "⟦0 < x; inv_end2 x ([], Oc # list)⟧ ⟹
               inv_end4 x ([], Bk # Oc # list)"
  by (auto simp: inv_end2.simps inv_end4.simps)

lemma inv_end4_Oc_via_2[elim]:  "⟦0 < x; inv_end2 x (b, Oc # list); b ≠ []⟧ ⟹
  inv_end4 x (tl b, hd b # Oc # list)"
  by(auto simp: inv_end2.simps inv_end4.simps gr0_conv_Suc)

lemma inv_end2_Oc_via_3[elim]: "⟦0 < x; inv_end3 x (b, Oc # list)⟧ ⟹ inv_end2 x (Oc # b, list)"
  by (auto simp: inv_end2.simps inv_end3.simps)

lemma inv_end4_Bk_via_Oc[elim]: "⟦0 < x; inv_end4 x (b, Oc # list)⟧ ⟹ inv_end4 x (b, Bk # list)"
  by (auto simp: inv_end2.simps inv_end4.simps)

lemma inv_end5_Bk_drop_Oc[elim]: "⟦0 < x; inv_end5 x ([], Oc # list)⟧ ⟹ inv_end5 x ([], Bk # Oc # list)"
  by (auto simp: inv_end2.simps inv_end5.simps)

declare inv_end5_loop.simps[simp del]
  inv_end5_exit.simps[simp del]

lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
  by (auto simp: inv_end5_exit.simps)

lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
  by (auto simp: inv_end5_loop.simps)

lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
  "⟦0 < x; inv_end5_loop x (b, Oc # list); b ≠ []; hd b = Bk⟧ ⟹
  inv_end5_exit x (tl b, Bk # Oc # list)"
  apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
  using hd_replicate apply fastforce
  by (metis cell.distinct(1) hd_append2 hd_replicate list.sel(3) self_append_conv2
      split_head_repeat(2))

lemma inv_end5_loop_Oc_Oc_drop[elim]: 
  "⟦0 < x; inv_end5_loop x (b, Oc # list); b ≠ []; hd b = Oc⟧ ⟹
  inv_end5_loop x (tl b, Oc # Oc # list)"
  apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
  apply(erule_tac exE)+
  apply(rename_tac i j)
  apply(rule_tac x = "i - 1" in exI, 
      rule_tac x = "Suc j" in exI, auto)
   apply(case_tac [!] i, simp_all)
  done

lemma inv_end5_Oc_tail[elim]: "⟦0 < x; inv_end5 x (b, Oc # list); b ≠ []⟧ ⟹ 
  inv_end5 x (tl b, hd b # Oc # list)"
  apply(simp add: inv_end2.simps inv_end5.simps)
  apply(case_tac "hd b", simp_all, auto)
  done

lemma inv_end_step:
  "⟦x > 0; inv_end x cf⟧ ⟹ inv_end x (step cf (tcopy_end, 0))"
  apply(cases cf, cases "snd (snd cf)"; cases "hd (snd (snd cf))")
     apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
  done

lemma inv_end_steps:
  "⟦x > 0; inv_end x cf⟧ ⟹ inv_end x (steps cf (tcopy_end, 0) stp)"
  apply(induct stp, simp add:steps.simps, simp)
  apply(erule_tac inv_end_step, simp)
  done

fun end_state :: "config ⇒ nat"
  where
    "end_state (s, l, r) = 
       (if s = 0 then 0
        else if s = 1 then 5
        else if s = 2 ∨ s = 3 then 4
        else if s = 4 then 3 
        else if s = 5 then 2
        else 0)"

fun end_stage :: "config ⇒ nat"
  where
    "end_stage (s, l, r) = 
          (if s = 2 ∨ s = 3 then (length r) else 0)"

fun end_step :: "config ⇒ nat"
  where
    "end_step (s, l, r) = 
         (if s = 4 then (if hd r = Oc then 1 else 0)
          else if s = 5 then length l
          else if s = 2 then 1
          else if s = 3 then 0
          else 0)"

definition end_LE :: "(config × config) set"
  where
    "end_LE = measures [end_state, end_stage, end_step]"

lemma wf_end_le: "wf end_LE"
  unfolding end_LE_def by auto

lemma halt_lemma: 
  "⟦wf LE; ∀n. (¬ P (f n) ⟶ (f (Suc n), (f n)) ∈ LE)⟧ ⟹ ∃n. P (f n)"
  by (metis wf_iff_no_infinite_down_chain)

lemma end_halt: 
  "⟦x > 0; inv_end x (Suc 0, l, r)⟧ ⟹ 
      ∃ stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
proof(rule halt_lemma[OF wf_end_le])
  assume great: "0 < x"
    and inv_start: "inv_end x (Suc 0, l, r)"
  show "∀n. ¬ is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) ⟶ 
    (steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) ∈ end_LE"
  proof(rule_tac allI, rule_tac impI)
    fix n
    assume notfinal: "¬ is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"
    obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"
      apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)
      done
    hence "inv_end x (s', l', r') ∧ s' ≠ 0"
      using great inv_start notfinal
      apply(drule_tac stp = n in inv_end_steps, auto)
      done
    hence "(step (s', l', r') (tcopy_end, 0), s', l', r') ∈ end_LE"
      apply(cases r'; cases "hd r'")
         apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits)
      done
    thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 
      steps (Suc 0, l, r) (tcopy_end, 0) n) ∈ end_LE"
      using d
      by simp
  qed
qed

lemma end_correct:
  "n > 0 ⟹ {inv_end1 n} tcopy_end {inv_end0 n}"
proof(rule_tac Hoare_haltI)
  fix l r
  assume h: "0 < n"
    "inv_end1 n (l, r)"
  then have "∃ stp. is_final (steps0 (1, l, r) tcopy_end stp)"
    by (simp add: end_halt inv_end.simps)
  then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
  moreover have "inv_end n (steps0 (1, l, r) tcopy_end stp)"
    apply(rule_tac inv_end_steps)
    using h by(simp_all add: inv_end.simps)
  ultimately show
    "∃stp. is_final (steps (1, l, r) (tcopy_end, 0) stp) ∧ 
    inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"        
    using h
    apply(rule_tac x = stp in exI)
    apply(cases "(steps0 (1, l, r) tcopy_end stp)") 
    apply(simp add: inv_end.simps)
    done
qed

(* tcopy *)

lemma tm_wf_tcopy[intro]:
  "tm_wf (tcopy_begin, 0)"
  "tm_wf (tcopy_loop, 0)"
  "tm_wf (tcopy_end, 0)"
  by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)

lemma tcopy_correct1: 
  assumes "0 < x"
  shows "{inv_begin1 x} tcopy {inv_end0 x}"
proof -
  have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
    by (metis assms begin_correct) 
  moreover 
  have "inv_begin0 x ↦ inv_loop1 x"
    unfolding assert_imp_def
    unfolding inv_begin0.simps inv_loop1.simps
    unfolding inv_loop1_loop.simps inv_loop1_exit.simps
    apply(auto simp add: numeral Cons_eq_append_conv)
    by (rule_tac x = "Suc 0" in exI, auto)
  ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"
    by (rule_tac Hoare_consequence) (auto)
  moreover
  have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
    by (metis assms loop_correct) 
  ultimately 
  have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
    by (rule_tac Hoare_plus_halt) (auto)
  moreover 
  have "{inv_end1 x} tcopy_end {inv_end0 x}"
    by (metis assms end_correct) 
  moreover 
  have "inv_loop0 x = inv_end1 x"
    by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
  ultimately 
  show "{inv_begin1 x} tcopy {inv_end0 x}"
    unfolding tcopy_def
    by (rule_tac Hoare_plus_halt) (auto)
qed

abbreviation (input)
  "pre_tcopy n ≡ λtp. tp = ([]::cell list, Oc ↑ (Suc n))"
abbreviation (input)
  "post_tcopy n ≡ λtp. tp= ([Bk], <(n, n::nat)>)"

lemma tcopy_correct:
  shows "{pre_tcopy n} tcopy {post_tcopy n}"
proof -
  have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
    by (rule tcopy_correct1) (simp)
  moreover
  have "pre_tcopy n = inv_begin1 (Suc n)"
    by (auto)
  moreover
  have "inv_end0 (Suc n) = post_tcopy n"
    unfolding fun_eq_iff
    by (auto simp add: inv_end0.simps tape_of_nat_def tape_of_prod_def)
  ultimately
  show "{pre_tcopy n} tcopy {post_tcopy n}" 
    by simp
qed


section ‹The {\em Dithering} Turing Machine›

text ‹
  The {\em Dithering} TM, when the input is ‹1›, it will loop forever, otherwise, it will
  terminate.
›

definition dither :: "instr list"
  where
    "dither ≡ [(W0, 1), (R, 2), (L, 1), (L, 0)] "

(* invariants of dither *)
abbreviation (input)
  "dither_halt_inv ≡ λtp. ∃k. tp = (Bk ↑ k, <1::nat>)"

abbreviation (input)
  "dither_unhalt_inv ≡ λtp. ∃k. tp = (Bk ↑ k, <0::nat>)"

lemma dither_loops_aux: 
  "(steps0 (1, Bk ↑ m, [Oc]) dither stp = (1, Bk ↑ m, [Oc])) ∨ 
   (steps0 (1, Bk ↑ m, [Oc]) dither stp = (2, Oc # Bk ↑ m, []))"
  apply(induct stp)
   apply(auto simp: steps.simps step.simps dither_def numeral)
  done

lemma dither_loops:
  shows "{dither_unhalt_inv} dither ↑" 
  apply(rule Hoare_unhaltI)
  using dither_loops_aux
  apply(auto simp add: numeral tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma dither_halts_aux: 
  shows "steps0 (1, Bk ↑ m, [Oc, Oc]) dither 2 = (0, Bk ↑ m, [Oc, Oc])"
  unfolding dither_def
  by (simp add: steps.simps step.simps numeral)

lemma dither_halts:
  shows "{dither_halt_inv} dither {dither_halt_inv}" 
  apply(rule Hoare_haltI)
  using dither_halts_aux
  apply(auto simp add: tape_of_nat_def)
  by (metis (lifting, mono_tags) holds_for.simps is_final_eq)


section ‹The diagnal argument below shows the undecidability of Halting problem›

text ‹
  ‹halts tp x› means TM ‹tp› terminates on input ‹x›
  and the final configuration is standard.
›

definition halts :: "tprog0 ⇒ nat list ⇒ bool"
  where
    "halts p ns ≡ {(λtp. tp = ([], <ns>))} p {(λtp. (∃k n l. tp = (Bk ↑ k,  <n::nat> @ Bk ↑ l)))}"

lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
  by (auto simp: tcopy_def)

lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
  by (auto simp: tm_wf.simps dither_def)

text ‹
  The following locale specifies that TM ‹H› can be used to solve 
  the {\em Halting Problem} and ‹False› is going to be derived 
  under this locale. Therefore, the undecidability of {\em Halting Problem}
  is established. 
›

locale uncomputable = 
  (* The coding function of TM, interestingly, the detailed definition of this 
  funciton @{text "code"} does not affect the final result. *)
  fixes code :: "instr list ⇒ nat" 
    (* 
  The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
  *)
    and H :: "instr list"
  assumes h_wf[intro]: "tm_wf0 H"
    (*
  The following two assumptions specifies that @{text "H"} does solve the Halting problem.
  *)
    and h_case: 
    "⋀ M ns. halts M ns ⟹ {(λtp. tp = ([Bk], <(code M, ns)>))} H {(λtp. ∃k. tp = (Bk ↑ k, <0::nat>))}"
    and nh_case: 
    "⋀ M ns. ¬ halts M ns ⟹ {(λtp. tp = ([Bk], <(code M, ns)>))} H {(λtp. ∃k. tp = (Bk ↑ k, <1::nat>))}"
begin

(* invariants for H *)
abbreviation (input)
  "pre_H_inv M ns ≡ λtp. tp = ([Bk], <(code M, ns::nat list)>)"

abbreviation (input)
  "post_H_halt_inv ≡ λtp. ∃k. tp = (Bk ↑ k, <1::nat>)"

abbreviation (input)
  "post_H_unhalt_inv ≡ λtp. ∃k. tp = (Bk ↑ k, <0::nat>)"


lemma H_halt_inv:
  assumes "¬ halts M ns" 
  shows "{pre_H_inv M ns} H {post_H_halt_inv}"
  using assms nh_case by auto

lemma H_unhalt_inv:
  assumes "halts M ns" 
  shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
  using assms h_case by auto

(* TM that produces the contradiction and its code *)

definition
  "tcontra ≡ (tcopy |+| H) |+| dither"
abbreviation
  "code_tcontra ≡ code tcontra"

(* assume tcontra does not halt on its code *)
lemma tcontra_unhalt: 
  assumes "¬ halts tcontra [code tcontra]"
  shows "False"
proof -
  (* invariants *)
  define P1 where "P1 ≡ λtp. tp = ([]::cell list, <code_tcontra>)"
  define P2 where "P2 ≡ λtp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
  define P3 where "P3 ≡ λtp. ∃k. tp = (Bk ↑ k, <1::nat>)"

(*
  {P1} tcopy {P2}  {P2} H {P3} 
  ----------------------------
     {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
  ------------------------------------------------
                 {P1} tcontra {P3}
  *)

  have H_wf: "tm_wf0 (tcopy |+| H)" by auto

(* {P1} (tcopy |+| H) {P3} *)
  have first: "{P1} (tcopy |+| H) {P3}" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tcopy *)
    show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
      by (rule tcopy_correct)
  next
    case B_halt (* of H *)
    show "{P2} H {P3}"
      unfolding P2_def P3_def 
      using H_halt_inv[OF assms]
      by (simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* {P3} dither {P3} *)
  have second: "{P3} dither {P3}" unfolding P3_def 
    by (rule dither_halts)

(* {P1} tcontra {P3} *)
  have "{P1} tcontra {P3}" 
    unfolding tcontra_def
    by (rule Hoare_plus_halt[OF first second H_wf])

  with assms show "False"
    unfolding P1_def P3_def
    unfolding halts_def
    unfolding Hoare_halt_def 
    apply(auto) apply(rename_tac n)
    apply(drule_tac x = n in spec)
    apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
    apply(auto simp add: tape_of_list_def)
    by (metis append_Nil2 replicate_0)
qed

(* asumme tcontra halts on its code *)
lemma tcontra_halt: 
  assumes "halts tcontra [code tcontra]"
  shows "False"
proof - 
  (* invariants *)
  define P1 where "P1 ≡ λtp. tp = ([]::cell list, <code_tcontra>)"
  define P2 where "P2 ≡ λtp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
  define Q3 where "Q3 ≡ λtp. ∃k. tp = (Bk ↑ k, <0::nat>)"

(*
  {P1} tcopy {P2}  {P2} H {Q3} 
  ----------------------------
     {P1} (tcopy |+| H) {Q3}     {Q3} dither loops
  ------------------------------------------------
               {P1} tcontra loops
  *)

  have H_wf: "tm_wf0 (tcopy |+| H)" by auto

(* {P1} (tcopy |+| H) {Q3} *)
  have first: "{P1} (tcopy |+| H) {Q3}" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tcopy *)
    show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
      by (rule tcopy_correct)
  next
    case B_halt (* of H *)
    then show "{P2} H {Q3}"
      unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
      by(simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* {P3} dither loops *)
  have second: "{Q3} dither ↑" unfolding Q3_def 
    by (rule dither_loops)

(* {P1} tcontra loops *)
  have "{P1} tcontra ↑" 
    unfolding tcontra_def
    by (rule Hoare_plus_unhalt[OF first second H_wf])

  with assms show "False"
    unfolding P1_def
    unfolding halts_def
    unfolding Hoare_halt_def Hoare_unhalt_def
    by (auto simp add: tape_of_list_def)
qed


text ‹
  ‹False› can finally derived.
›

lemma false: "False"
  using tcontra_halt tcontra_unhalt 
  by auto

end

declare replicate_Suc[simp del]

end